Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
Identifieur interne : 001512 ( Main/Exploration ); précédent : 001511; suivant : 001513Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
Auteurs : Ralf Karrenberg [Allemagne] ; Marek Košta [Allemagne] ; Thomas Sturm [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today’s computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.
Url:
DOI: 10.1007/978-3-642-40885-4_5
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001297
- to stream Istex, to step Curation: 001280
- to stream Istex, to step Checkpoint: 000138
- to stream Hal, to step Corpus: 003C81
- to stream Hal, to step Curation: 003C81
- to stream Hal, to step Checkpoint: 000F24
- to stream Main, to step Merge: 001524
- to stream Main, to step Curation: 001512
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages</title><author><name sortKey="Karrenberg, Ralf" sort="Karrenberg, Ralf" uniqKey="Karrenberg R" first="Ralf" last="Karrenberg">Ralf Karrenberg</name></author><author><name sortKey="Kosta, Marek" sort="Kosta, Marek" uniqKey="Kosta M" first="Marek" last="Košta">Marek Košta</name></author><author><name sortKey="Sturm, Thomas" sort="Sturm, Thomas" uniqKey="Sturm T" first="Thomas" last="Sturm">Thomas Sturm</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:50BFA42D4BE590F6051D477523C174E311104AA3</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-40885-4_5</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-1PXKFMMF-8/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001297</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001297</idno><idno type="wicri:Area/Istex/Curation">001280</idno><idno type="wicri:Area/Istex/Checkpoint">000138</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000138</idno><idno type="wicri:doubleKey">0302-9743:2013:Karrenberg R:presburger:arithmetic:in</idno><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-00931954</idno><idno type="url">https://hal.inria.fr/hal-00931954</idno><idno type="wicri:Area/Hal/Corpus">003C81</idno><idno type="wicri:Area/Hal/Curation">003C81</idno><idno type="wicri:Area/Hal/Checkpoint">000F24</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000F24</idno><idno type="wicri:Area/Main/Merge">001524</idno><idno type="wicri:Area/Main/Curation">001512</idno><idno type="wicri:Area/Main/Exploration">001512</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages</title><author><name sortKey="Karrenberg, Ralf" sort="Karrenberg, Ralf" uniqKey="Karrenberg R" first="Ralf" last="Karrenberg">Ralf Karrenberg</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Saarland University, 66123, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Kosta, Marek" sort="Kosta, Marek" uniqKey="Kosta M" first="Marek" last="Košta">Marek Košta</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max-Planck-Institut für Informatik, 66123, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Sturm, Thomas" sort="Sturm, Thomas" uniqKey="Sturm T" first="Thomas" last="Sturm">Thomas Sturm</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Max-Planck-Institut für Informatik, 66123, Saarbrücken</wicri:regionArea><placeName><region type="land" nuts="2">Sarre (Land)</region><settlement type="city">Sarrebruck</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today’s computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>Sarre (Land)</li></region><settlement><li>Sarrebruck</li></settlement></list><tree><country name="Allemagne"><region name="Sarre (Land)"><name sortKey="Karrenberg, Ralf" sort="Karrenberg, Ralf" uniqKey="Karrenberg R" first="Ralf" last="Karrenberg">Ralf Karrenberg</name></region><name sortKey="Karrenberg, Ralf" sort="Karrenberg, Ralf" uniqKey="Karrenberg R" first="Ralf" last="Karrenberg">Ralf Karrenberg</name><name sortKey="Kosta, Marek" sort="Kosta, Marek" uniqKey="Kosta M" first="Marek" last="Košta">Marek Košta</name><name sortKey="Kosta, Marek" sort="Kosta, Marek" uniqKey="Kosta M" first="Marek" last="Košta">Marek Košta</name><name sortKey="Sturm, Thomas" sort="Sturm, Thomas" uniqKey="Sturm T" first="Thomas" last="Sturm">Thomas Sturm</name><name sortKey="Sturm, Thomas" sort="Sturm, Thomas" uniqKey="Sturm T" first="Thomas" last="Sturm">Thomas Sturm</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001512 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 001512 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:50BFA42D4BE590F6051D477523C174E311104AA3
|texte= Presburger Arithmetic in Memory Access Optimization for Data-Parallel Languages
}}
| This area was generated with Dilib version V0.6.33. |  |